Section: Scientific Foundations

Interactive proofs of programs

Participants : Sylvie Boldo, Évelyne Contejean, Jean-Christophe Filliâtre, Guillaume Melquiond, Christine Paulin-Mohring.

Higher-order strongly typed programming languages such as Objective Caml help improving the quality of software development. Static typing automatically detects possible execution errors. Higher-order functions, polymorphism, modules and functors are powerful tools for the development of generic reusable libraries. Our general goal is to enrich such a software environment with a language of annotations as well as libraries for datatypes, abstract notions and associated theorems which can express logical properties of programs and ease the possibility to automatically and interactively develop proofs of correctness of the programs.

In the past, we made contributions to the Coq proof assistant by adding functionalities for improving the development of formally proved functional programs. A first contribution is a new method to extract OCaml modular code from Coq proofs (P. Letouzey PhD thesis [80] , [81] ). This extraction mechanism is an original feature for the Coq system, and has been used by several teams around the world in order to get efficient certified code  [78] . Another contribution (M. Sozeau PhD thesis  [91] , [92] ) is an extension of the Coq input language for building programs with strong specifications by writing only the computational part and generating separately proof obligations (which are usually solved by tactics) and also a mechanism generalizing Type Classes à la Haskell which gives overloading in programs and proofs and facilitates the development of generic tactics..

We are using the capability of the Coq system to model both computation and deduction in order to explore different classes of applications. These examples involve the development of large reusable Coq libraries and suggest domain-specific specification and proof strategies.

Randomized algorithms

C. Paulin in collaboration with Ph. Audebaud from ENS Lyon, proposed a method for modeling probabilistic programs in Coq  [49] . The method is based on a monadic interpretation of probabilistic programs as probability measures. A large Coq library has been developed and made publicly available (see also Section 5.12 ). D. Baelde has been using this library to formally prove the security of Watermarking algorithms (see also section 6.1 ).

Floating-point programs

Many industrial programs (weather forecasts, plane trajectories, simulations...) use floating-point computations, typically double precision floating-point numbers  [93] . Even if each computation is as good as it can be (except for elementary functions like sine, or exponential), the final result may be very wrong with no warnings, or the program will produce unexpected behaviors (like division by zero). This is the reason why guarantees should be provided to the user. We mean to guarantee for example that, for all or part of the possible inputs, the result obtained is correct (or near enough) and that no exceptional behavior will occur  [55] .

A high level of guarantee is obtained by formal proofs in Coq. We maintain and develop large Coq libraries for floating-point arithmetic: core definitions, axiomatic and computational rounding operations, high-level properties. It provides a framework for developers to formally certify numerical applications. A new such library is described in Section  5.9 .

Certification of tools

Certifying the result of tools for analysing programs is a good challenge in the domain of proofs of higher-order functional programs. We obtained several results concerning formal proofs in Coq corresponding to automated deduction. These results are described in Section  3.3 .

A PhD thesis started in Sep. 2009 has for main objective the development of a certified version the Frama-C/Jessie/Why verification chain.